PL conferences:
@STRING{esop = "European Symposium on Programming (ESOP)"}
@STRING{cav = "Computer Aided Verification (CAV)"}
@STRING{concur = "International Conference on Concurrency Theory (CONCUR)"}
@STRING{pldi = "Programming Language Design and Implementation (PLDI)"} % ACM SIGPLAN Conference on 
@STRING{sas = "Static Analysis Symposium (SAS)"}
@STRING{ppopp = "Symposium on Principles and Practice of Parallel Programming (PPoPP)"} %ACM SIGPLAN 
@STRING{popl = "Principles of Programming Languages (POPL)"} %ACM SIGPLAN-SIGACT Symposium on 
@STRING{icfp = "International Conference on Functional Programming (ICFP)"} % ACM SIGPLAN
@STRING{oopsla = "Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)"}
@STRING{haskell = "Haskell Symposium"}
@STRING{tacas = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"}
@STRING{asplos = "International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)"}
@STRING{rv = "International Workshop on Runtime Verification (RV)"}
@STRING{vmcai = "International Conference on Verification, Model Checking, and Abstract Interpretation"}
@STRING{padtad = "Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD)"}
@STRING{woda = "International Workshop on Dynamic Analysis (WODA)"}
@STRING{tldi = "Workshop on Types in Language Design and Implementation (TLDI)"}
@STRING{lfp = "{ACM} Conference on Lisp and Functional Programming"}
@STRING{spin = "International SPIN Workshop on Model Checking of Software"}
@STRING{issta = "International Symposium on Software Testing and Analysis (ISSTA)"}
@string{paste="Program Analysis for Software Tools and Engineering (PASTE)"}
@string{pepm="Workshop on Partial Evaluation and Program Manipulation (PEPM)"}

OS conferences:
@STRING{sosp = "ACM Symposium on Operating Systems Principles (SOSP)"}
@STRING{osdi = "Operating Systems Design and Implementation (OSDI)"}
@STRING{hotos= "Workshop on Hot Topics in Operating Systems (HOTOS)"}
@STRING{ecrts= "Euromicro Conference on Real-Time Systems (ECRTS)"}


SE conferences:
@STRING{fse = "International Symposium on Foundations of Software Engineering (FSE)"} %ACM SIGSOFT
@STRING{icse = "International Conference on Software Engineering (ICSE)"}
@STRING{fase = "International Conference on Fundamental Approaches to Software Engineering (FASE)"}
@STRING{ase = "International Conference on Automated Software Engineering (ASE)"}
@STRING{podc = "ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC)"}

Architecture conferences:
@STRING{isca = "International Symposium on Computer Architecture (ISCA)"}

Journals:
@STRING{toplas = "Transactions on Programming Languages and Systems (TOPLAS)"}
@STRING{tse = "IEEE Transactions on Software Engineering"}
@STRING{jsl = "Journal of Symbolic Logic"}
@STRING{loplas = "ACM Letters on Programming Languages and Systems (LOPLAS)"}
@STRING{tocs = "ACM Transactions on Computer Systems (TOCS)"}
@STRING{scp = "Science of Computer Programming"}

Other:
@STRING{lncs = "Lecture Notes in Computer Science"}
@STRING{tr = "Technical Report"}
@STRING{sigplan = "SIGPLAN Notices"}
@STRING{springer = "Springer-Verlag"}
@STRING{acm = "ACM"}
@STRING{cacm = "Communications of the ACM"}

@INPROCEEDINGS{Berenson:snapshot,
 author = {H. Berenson and P. Bernstein and J. Gray and J. Melton and E. O'Neil and P. O'Neil},
 title = {A critique of ANSI SQL isolation levels},
 booktitle = {SIGMOD '95: International Conference on Management of Data},
 year = {1995},
 pages = {1--10},
 location = {San Jose, California, United States}
}

@INPROCEEDINGS{Burckhardt:semantics,
  author={Burckhardt, Sebastian and Leijen, Daan},
  title={{S}emantics of {C}oncurrent {R}evisions},
  booktitle={European Symposium on Programming (ESOP), \textrm{LNCS}},
  year=2011,
  volume={6602},
  pages={116--135}
}

@ARTICLE{Fekete:snapshot,
  author = {A. Fekete and D. Liarokapis and E. O'Neil and P. O'Neil and D. Shasha},
 title = {Making snapshot isolation serializable},
 journal = {ACM Trans. Database Syst.},
 volume = {30},
 number = {2},
 year = {2005},
 issn = {0362-5915},
 pages = {492--528}
}

@INPROCEEDINGS{Burckhardt:revisions,
  author   = {S. Burckhardt and A. Baldassin and D. Leijen},
  title    = {Concurrent Programming with Revisions and Isolation Types},
  booktitle= {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
  year     = 2010,
  _month    = Oct,
  _location = {Reno, Nevada},
}



@InProceedings{welc-saha-tabatabai-SPAA08,
  author = {A. Welc and B. Saha and A.-R. Adl-Tabatabai},
  title = 	 {Irrevocable transactions and their applications},
  year = 	 {2008},
  booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
  pages = {285--296}
}

@article{hanlon07,
 author = {C. O'Hanlon},
 title = {A Conversation with {J}ohn {H}ennessy and {D}avid {P}atterson},
 journal = {Queue},
 volume = {4},
 number = {10},
 year = {2007},
 pages = {14--22}
}

@book{larus07book,
 author = {J. Larus and R. Rajwar},
 title = {Transactional Memory},
 publisher = {Morgan \& Claypool Publishers},
 year = {2007}
}

@book{ hatton04book,
 author = {E. Hatton and A. S. Lobao and D. Weller},
 title = {Beginning .{NET} Game Programming in C\#},
 publisher = {Apress},
 year = {2004}
}


@inproceedings{martin-birrell-harris-isard-POPL08,
 author = {A. Martin and A. Birrell and T. Harris and M. Isard},
 title = {Semantics of transactional memory and automatic mutual exclusion},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2008},
 pages = {63--74},
 doi = {\url{http://doi.acm.org/10.1145/1328438.1328449}},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@inproceedings{acar-ahmed-blume-POPL08,
 author = {U. Acar and A. Ahmed and M. Blume},
 title = {Imperative self-adjusting computation},
 booktitle = popl,
 year = {2008},
}

@inproceedings{lee-et-al-ASPLOS2010,
 author = {D. Lee and B. Wester and K. Veeraraghavan and S. Narayanasamy and P. Chen and J. Flinn},
 title = {Respec: Efficient Online Multiprocessor Replay via Speculation and External Determinism},
 booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
 year = {2010},
 }

@inproceedings{yahav-POPL01,
 author = {E. Yahav},
 title = {Verifying safety properties of concurrent {Java} programs using 3-valued logic},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2001},
 dont_isbn = {1-58113-336-7},
 pages = {27--40},
 dont_location = {London, United Kingdom},
 dont_doi = {\url{http://doi.acm.org/10.1145/360204.360206}},
 dont_publisher = {ACM Press},
}

@inproceedings{koskinen-parkinson-herlihy-POPL10,
 author = {E. Koskinen and M. Parkinson and M. Herlihy},
 title = {Coarse-grained transactions},
 booktitle = popl,
 year = {2010},
 dont_isbn = {978-1-60558-479-9},
 _pages = {19--30},
 dont_location = {Madrid, Spain},
 dont_doi = {http://doi.acm.org/10.1145/1706299.1706304},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@inproceedings{lee-palsberg-ppopp2010,
 author = {J. Lee and J. Palsberg},
 title = {Featherweight X10: a core calculus for async-finish parallelism},
 booktitle = {Principles and Practice of Parallel Programming (PPoPP)},
 year = {2010},
 }


@inproceedings{herlihy-koskinen-PPOPP08,
 author = {M. Herlihy and E. Koskinen},
 title = {Transactional boosting: a methodology for highly-concurrent transactional objects},
 booktitle = {Principles and Practice of Parallel Programming (PPoPP)},
 year = {2008},
 isbn = {978-1-59593-795-7},
 _pages = {207--216},
 dont_location = {Salt Lake City, UT, USA},
 dont_doi = {http://doi.acm.org/10.1145/1345206.1345237},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@inproceedings{vafeiadis-herlihy-hoare-shapiro-PPOPP06,
 author = {V. Vafeiadis and M. Herlihy and T. Hoare and M. Shapiro},
 title = {Proving correctness of highly-concurrent linearisable objects},
 booktitle = {Principles and Practice of Parallel Programming (PPoPP)},
 year = {2006},
 dont_isbn = {1-59593-189-9},
 pages = {129--136},
 dont_location = {New York, New York, USA},
 dont_doi = {http://doi.acm.org/10.1145/1122971.1122992},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }


@inproceedings{scott07iiswc,
 author = {M. Scott and M. Spear and L. Dalessandro and V. Marathe},
 title = {Delaunay Triangulation with Transactions and Barriers},
 booktitle = {{IEEE} International Symposium on Workload Characterization},
 year = {2007},
 pages = {107--113}
}

@inproceedings{watson07pact,
 author = {I. Watson and C. Kirkham and M. Lujan},
 title = {A Study of a Transactional Parallel Routing Algorithm},
 booktitle = {International Conference on Parallel Architectures and Compilation Techniques},
 year = {2007},
 pages = {388--398}
}

@article{rhal06lncs,
 author = {A. El Rhalibi and M. Merabti and Y Shen},
 title = {Improving Game Processing in Multithreading and Multiprocessor Architecture},
 journal = {Lecture Notes in Computer Science},
 year = {2006},
 volume = {3942},
 pages = {669--679}
}

@InProceedings{rinard-diniz,
  author =       {M. Rinard and P. Diniz},
  title =        {Eliminating Synchronization Bottlenecks in Object-Based Programs Using Adaptive Replication},
  year =      {1999},
  booktitle =    {International Conference on Supercomputing },
}

@inproceedings{aydo08transact,
 author = {U. Aydonat and T. Abdelrahman},  
title = {Serializability of Transactions in Software Transactional Memory},
  booktitle = {Workshop on Transactional Computing (TRANSACT)}, 
 year = {2008}
 }
@inproceedings{riegel-fetzer-felber-TRANSACT06,
   author = {T. Riegel and C. Fetzer and P. Felber},  
   title = {Snapshot Isolation for Software Transactional Memory},
   booktitle = {Workshop on Transactional Computing (TRANSACT)}, 
   year = {2006}
}



@techreport{ blund06trep,
 author = {C. Blundell and E. Lewis and M. Martin}, 
 title = {Unrestricted Transactional Memory: Supporting {I/O} and System Calls within Transactions},  
institution = {University of Pennsylvania},  
year = {2006},  
number = {TR-CIS-06-09} 
}



@techreport{ companionTR,
 author = {S. Burckhardt and D. Leijen}, 
 title = {Semantics of Concurrent Revisions (Full Version)},  
institution = {Microsoft},  
year = {2010},  
number = {MSR-TR-2010-94} 
}




@article{fraser-harris-TOCS07,
 author = {K. Fraser and T. Harris},
 title = {Concurrent programming without locks},
 journal = {ACM Trans. Comput. Syst.},
 volume = {25},
 number = {2},
 year = {2007},
 issn = {0734-2071},
 pages = {5},
 doi = {http://doi.acm.org/10.1145/1233307.1233309},
 publisher = {ACM Press},
 address = {New York, NY, USA},
}

@Misc{leiserson-prokop-98,
  OPTkey = 	 {},
  author = 	 {C. E. Leiserson and H. Prokop},
  title = 	 {A Minicourse on Multithreaded Programming},
  OPThowpublished = {},
  OPTmonth = 	 {},
  year = 	 {1998},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@inproceedings{frigo-halpern-leiserson-lewin-berlin-SPAA09,
 author = {M. Frigo and P. Halpern and C. E. Leiserson and S. Lewin-Berlin},
 title = {Reducers and other {C}ilk++ hyperobjects},
 booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
 year = {2009},
 dont_isbn = {978-1-60558-606-9},
 _pages = {79--90},
 dont_location = {Calgary, AB, Canada},
 dont_doi = {http://doi.acm.org/10.1145/1583991.1584017},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@inproceedings{park-dill-SPAA95,
 author = {S. Park and D. L. Dill},
 title = {An executable specification, analyzer and verifier for {RMO} (relaxed memory order)},
 booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
 year = {1995},
 isbn = {0-89791-717-0},
 pages = {34--41},
 dont_location = {Santa Barbara, California, United States},
 dont_doi = {http://doi.acm.org/10.1145/215399.215413},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@inproceedings{doherty-et-al-SPAA04,
 author = {S. Doherty and D. Detlefs and L. Grove and C. Flood and V. Luchangco and P. Martin and M. Moir and N. Shavit and G. Steele},
 title = {{DCAS} is not a silver bullet for nonblocking algorithm design},
 booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
 year = {2004},
 isbn = {1-58113-840-7},
 pages = {216--224},
 dont_location = {Barcelona, Spain},
 doi = {http://doi.acm.org/10.1145/1007912.1007945},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
} 

@inproceedings{dill-park-nowatzyk-93,
 author = {D. Dill and S. Park and A. Nowatzyk},
 title = {Formal specification of abstract memory models},
 booktitle = {Symposium on Research on Integrated Systems},
 year = {1993},
 isbn = {0-262-02357-1},
 pages = {38--52},
 dont_location = {Seattle, Washington, United States},
 publisher = {MIT Press},
 dont_address = {Cambridge, MA, USA},
 }

@article{ savage-et-al-TCS97,
    author = "S. Savage and M. Burrows and G. Nelson and P. Sobalvarro and T. Anderson",
    title = "{Eraser}: {A} Dynamic Data Race Detector for Multithreaded Programs",
    journal = "ACM Trans. Comp. Sys.",
    volume = "15",
    number = "4",
    pages = "391--411",
    year = "1997",
    url = "citeseer.ist.psu.edu/article/savage97eraser.html" 
}

@Article{morrison-MSDN05,
  author =       {V. Morrison},
  title =        {Understand the Impact of Low-Lock Techniques in Multithreaded Apps},
  journal =      {MSDN Magazine},
  year =         {2005},
  volume =    {20},
  number =    {10},
  month =     {October},
}

@article{larus-CACM09,
 author = {J. Larus},
 title = {Spending Moore's Dividend},
 journal = {Commun. ACM},
 volume = {52},
 issue = {5},
 dont_month = {May},
 year = {2009},
 dont_issn = {0001-0782},
 pages = {62--69},
 dont_numpages = {8},
 dont_url = {http://doi.acm.org/10.1145/1506409.1506425},
 dont_doi = {http://doi.acm.org/10.1145/1506409.1506425},
 dont_acmid = {1506425},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
}


@article{sutter-larus-Q05,
 author = {H. Sutter and J. Larus},
 title = {Software and the concurrency revolution},
 journal = {ACM Queue},
 volume = {3},
 number = {7},
 year = {2005},
 issn = {1542-7730},
 pages = {54--62},
 doi = {http://doi.acm.org/10.1145/1095408.1095421},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@inproceedings{zhao-zhang-malik-DAC01,
 author = {M. Moskewicz and C. Madigan and Y. Zhao and L. Zhang and S. Malik},
 title = {{Chaff}: {Engineering} an efficient {SAT} solver},
 booktitle = {Design Automation Conference (DAC)},
 year = {2001},
 dont_isbn = {1-58113-297-2},
 pages = {530--535},
 dont_location = {Las Vegas, Nevada, United States},
 dont_doi = {http://doi.acm.org/10.1145/378239.379017},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@Manual{powerpc-arch-manual,
  title =        {{PowerPC} Architecture Book v2.02},
  author =    {B. Frey},
  organization = {International Business Machines Corporation},
  year =      {2005}
}

@Manual{z-manual,
  title =        {z/Architecture Principles of Operation},
  organization = {International Business Machines Corporation},
  edition =      {First},
  month =        {December},
  year =         {2000},
}

@Book{sparc-v9-manual,
  editor =       {D. Weaver and T. Germond},
  title =        {The SPARC Architecture Manual Version 9},
  publisher =    {PTR Prentice Hall},
  year =         {1994}
}

@Manual{alpha-manual,
  title =        {Alpha Architecture Reference Manual},
  organization = {Compaq Computer Corporation},
  edition =   {4th},
  month =     {January},
  year =      {2002},
}

@Manual{itanium-form-manual,
  title =        {A Formal Specification of the Intel Itanium Processor Family Memory Ordering},
  organization = {Intel Corporation},
  month =        {October},
  year =         {2002},
}

@Manual{itanium-manual,

  title =        {Intel Itanium Architecture Software Developer's Manual, Book 2, rev. 2.2},
  organization = {Intel Corporation},
  month =        {January},
  year =         {2006},
}

@Manual{amd-manual,
  title =        {AMD64 Architecture Programmer's Manual Volume 2: System Programming},
  organization = {AMD},
  month =        {September},
  year =         {2007},
}


@Manual{ia32-manual,
  title =        {Intel 64 and IA-32 Architectures Software Developer's Manual, Volume 3A},
  organization = {Intel Corporation},
  month =        {November},
  year =         {2006},
}

@Manual{ia64-whitepaper,
  title =        {Intel 64 Architecture Memory Ordering White Paper},
  organization = {Intel Corporation},
  month =        {August},
  year =         {2007},
}

@Manual{threading-building-blocks,
  title =        {Intel Threading Building Blocks},
  organization = {Intel Corporation},
  month =        {September},
  year =         {2006},
}

@InProceedings{cil,
  author =       {G. Necula and S. McPeak and S.P. Rahul and W. Weimer},
  title =        {{CIL}: Intermediate Language and Tools for Analysis and Transformation of {C} Programs},
  booktitle = {Conf. on Compiler Constr. (CC)},
  year =      {2002},
}


@book{collier-92,
 author = {W. W. Collier},
 title = {Reasoning about parallel architectures},
 year = {1992},
 isbn = {0-13-767187-3},
 publisher = {Prentice-Hall, Inc.},
 address = {Upper Saddle River, NJ, USA},
 }

@inproceedings{martin-et-al-MICRO01,
 author = {M. Martin and D. Sorin and H. Cain and M. Hill and M. Lipasti},
 title = {Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing},
 booktitle = {International Symposium on Microarchitecture (MICRO)},
 year = {2001},
 isbn = {0-7695-1369-7},
 pages = {328--337},
 dont_location = {Austin, Texas},
 dont_publisher = {ACM},
 dont_address = {Washington, DC, USA},
 }

@InProceedings{qadeer-rehof-TACAS05,
  author =       {S. Qadeer and J. Rehof},
  title =        {Context-bounded model checking of concurrent software},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  pages =     {93},
  year =      {2005},
  dont_editor =    {N. Halbwachs and L. D. Zuck},
  series =    {LNCS 3440},
  publisher = {Springer},
}

@article{pong-dubois-97,
    author = {F. Pong and M. Dubois},
    title = {Verification Techniques for Cache Coherence Protocols},
    journal = {ACM Computing Surveys},
    volume = {29},
    number = {1},
    pages = {82--126},
    year = {1997},
    url = {citeseer.ist.psu.edu/pong97verification.html}
}

@inproceedings{vafeiadis-VMCAI09,
  author = {V. Vafeiadis},
  title = {Shape-Value Abstraction for Verifying Linearizability},
  booktitle = {Verification, Model Checking and Abstract Interpretation (VMCAI)},
  publisher = {Springer-Verlag},
  year = {2009},
}


@Article{ papadimitriou-JACM79,
  author = 	 {C. H. Papadimitriou},
  title = 	 {The serializability of concurrent database updates},
  journal = 	 {J. ACM},
  year = 	 {1979},
  volume = 	 {26},
  number = 	 {4},
  month = 	 {October},
}

@Article{ huet-JACM80,
  author = 	 {G. Huet},
  title = 	 {Confluent Reductions: Abstract Properties and Applications in Term Rewriting Systems},
  journal = 	 {J. ACM},
  year = 	 {1980},
  volume = 	 {27},
  number = 	 {4},
  month = 	 {October},
}

@inproceedings{gopalakrishnan-yang-sivaraj-CAV04,
  author    = {G. Gopalakrishnan and
               Y. Yang and
               H. Sivaraj},
  title     = {{QB} or Not {QB}: An Efficient Execution Verification Tool for
               Memory Orderings.},
  booktitle = {Computer-Aided Verification (CAV)},
  year      = {2004},
  pages     = {401--413},
  series = {LNCS 3114},
  dont_ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3114{\&}spage=401},
  dont_bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{nalumasu-et-al-CAV04,
  author    = {R. Nalumasu and R. Ghugal and G. Gopalakrishnan and G. Lindstrom and K. Slind},
  title     = {The `test model-checking' approach to the verification of formal memory models of multiprocessors},
  booktitle = {Computer-Aided Verification (CAV)},
  year      = {1998},
  pages     = {464--476},
  series = {LNCS 1427},
}

@InProceedings{yang-gopalakrishnan-CHARME03, 
 author = {Y. Yang and  G. Gopalakrishnan and G. Lindstrom and K. Slind},
 title = {Analyzing the {Intel} {Itanium} Memory Ordering Rules Using Logic Programming and {SAT}},
 booktitle = {Correct Hardware Design and Verification Methods (CHARME)},
 pages = {81--95},
 year = {2003},
 dont_volume = {2860},
 series = {LNCS 2860},
 dont_month = {January}, 
 publisher = {Springer},
}

@article{yahav-sagiv-ENTCS89,
  author    = {E. Yahav and M. Sagiv},
  title     = {Automatically Verifying Concurrent Queue Algorithms.},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {89},
  number    = {3},
  year      = {2003},
  ee        = {http://www.elsevier.com/gej-ng/31/29/23/141/23/show/Products/notes/index.htt\#006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{elmas-tasiran-RV05,
  author    = {T. Elmas and S. Tasiran},
  title     = {{VyrdMC}: Driving Runtime Refinement Checking with Model Checkers},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  pages = {41--56},
  volume    = {144},
  year      = {2006},
}


@inproceedings{clarke-kroening-lerda-TACAS04,
  AUTHOR    = { E. Clarke
                and D. Kroening
                and F. Lerda},
  TITLE     = { A Tool for Checking {ANSI-C} Programs },
  BOOKTITLE = { Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  YEAR      = { 2004 },
  PUBLISHER = { Springer },
  pages     = { 168--176 },
  dont_ISBN      = { 3-540-21299-X },
  SERIES    = { LNCS 2988 },
  dont_VOLUME    = {  },
  dont_EDITOR    = { Kurt Jensen and Andreas Podelski },
}

@InProceedings{rabinovitz-grumberg-CAV05,
  author =       {I. Rabinovitz and O. Grumberg},
  title =        {Bounded Model Checking of Concurrent Programs},
  booktitle = {Computer-Aided Verification (CAV)},
  pages =     {82--97},
  year =      {2005},
  dont_editor =    {K. Etessami and S. K. Rajamani},
  dont_number =    {3576},
  series =    {LNCS 3576},
  dont_month =     {July},
  publisher = {Springer},
}

@InProceedings{yang-gopalakrishnan-PDPS04,
  author =       {Y. Yang and G. Gopalakrishnan and G. Lindstrom and K. Slind},
  title =        {Nemos: A framework for axiomatic and executable specifications of memory consistency models},
  doi =          {10.1109/IPDPS.2004.1302944},
  booktitle = {International Parallel and Distributed Processing Symposium (IPDPS)},
  dont_publisher = {IEEE},
  year =      {2004}
}


@article{prakash-lee-johnson-TC94,
  author =    {S. Prakash and  H. Yee and  T. Johnson},
  title =     {A Nonblocking Algorithm for Shared Queues Using Compare-and-Swap},
  journal =   {IEEE Trans. Comp.},
  year =      {1994},
  volume =    {43},
  number =    {5},
  pages =     {548--559},
  month =     {May},
}



@InProceedings{valois-PDCS94,
  author =    {J. Valois},
  title =     {Implementing Lock-Free Queues},
  booktitle = {Parallel and Distributed Computing and Systems (PDCS)},
  pages =     {64--69},
  year =      {1994},
  month =     {October},
}

@inproceedings{stone-PS90,
 author = {J. Stone},
 title = {A simple and correct shared-queue algorithm using compare-and-swap},
 booktitle = {Conference on Supercomputing},
 year = {1990},
 isbn = {0-89791-412-0},
 pages = {495--504},
 location = {New York, New York, United States},
 dont_publisher = {IEEE Computer Society Press},
 address = {Los Alamitos, CA, USA},
 }


@article{steinke-nutt-JACM04,
 author = {R. Steinke and G. Nutt},
 title = {A unified theory of shared memory consistency},
 journal = {J. ACM},
 volume = {51},
 number = {5},
 year = {2004},
 issn = {0004-5411},
 pages = {800--849},
 doi = {http://doi.acm.org/10.1145/1017460.1017464},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{adve-hill-TPDS93,
 author = {S. Adve and M. Hill},
 title = {A Unified Formalization of Four Shared-Memory Models},
 journal = {IEEE Trans. Parallel Distrib. Syst.},
 volume = {4},
 number = {6},
 year = {1993},
 issn = {1045-9219},
 pages = {613--624},
 doi = {http://dx.doi.org/10.1109/71.242161},
 dont_publisher = {IEEE Press},
 address = {Piscataway, NJ, USA},
 }

@inproceedings{kulkarni-et-al-PLDI07,
 author = {M. Kulkarni and K. Pingali and B. Walter and G. Ramanarayanan and K. Bala and L. Chew},
 title = {Optimistic parallelism requires abstractions},
 booktitle = pldi,
 year = {2007},
 }


@InProceedings{xu-bodik-hill-PLDI05,
  author =       {M. Xu and R. Bodik and M. Hill},
  title =        {A Serializability Violation Detector for Shared-Memory Server Programs},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year = {2005},
}

@InProceedings{flanagan-freund-yi-PLDI08,
  author =       {C. Flanagan and S. Freund and J.Yi},
  title =        {Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year = {2008},
}

@article{adve-gharachorloo-96,
 author = {S. Adve and K. Gharachorloo},
 title = {Shared Memory Consistency Models: a tutorial},
 journal = {Computer},
 volume = {29},
 number = {12},
 year = {1996},
 dont_issn = {0018-9162},
 pages = {66--76},
 dont_doi = {http://dx.doi.org/10.1109/2.546611},
 dont_publisher = {IEEE Computer Society Press},
 dont_address = {Los Alamitos, CA, USA},
 }


@InProceedings{berenson-bernstein-gray-melton-oneil-SIGMOD95,
  author = 	 {H. Berenson and P. Bernstein and J. Gray and J. Melton and E. O'Neil and P. O'Neil},
  title = 	 {A critique of {ANSI SQL} isolation levels},
  booktitle = {Proceedings of SIGMOD},
  pages = 	 {1--10},
  year = 	 {1995},
}

@article{bernstein-goodman-83,
 author = {P.A.Bernstein and N.Goodman},
 title = {Multiversion concurrency control---theory and algorithms},
 journal = {ACM Trans. Database Syst.},
 volume = {8},
 number = {4},
 year = {1983},
 dont_issn = {0362-5915},
 pages = {465--483},
 dont_doi = {http://doi.acm.org/10.1145/319996.319998},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }



@Book{bernstein-hadzilacos-goodman-87,
  author = 	 {P.A.Bernstein and V.Hadzilacos and N.Goodman},
  title = 	 {Concurrency Control and Recovery in Database Systems},
  publisher = 	 {Addison-Wesley},
  year = 	 {1987},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{alur-mcmillan-peled-LICS96,
  author =       {R. Alur and K. McMillan and D. Peled},
  title =        {Model-checking of correctness conditions for concurrent objects},
  booktitle = {Logic in Computer Science (LICS)},
  dont_publisher = {IEEE},
  pages =     {219--228},
  year =      {1996},
}

@article{herlihy-wing-TOPLAS90,
 author = {M. Herlihy and J. Wing},
 title = {Linearizability: a correctness condition for concurrent objects},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {12},
 number = {3},
 year = {1990},
 dont_issn = {0164-0925},
 pages = {463--492},
 dont_doi = {http://doi.acm.org/10.1145/78969.78972},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@article{lamport-79,
  author =       {L. Lamport},
  title =        {How to make a multiprocessor computer that correctly executes multiprocess programs},
  journal =      {IEEE Trans. Comp.},
  year =         {1979},
  volume =    {C-28},
  number =    {9},
  pages =     {690--691},
  dont_month =     {September},
}

@inproceedings{elmas-tasiran-qadeer-PLDI05,
  author = {T. Elmas and S. Tasiran and S. Qadeer},
  title = {{VYRD}: verifying concurrent programs by runtime refinement-violation detection},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year = {2005},
  dont_isbn = {1-59593-056-6},
  pages = {27--37},
  dont_location = {Chicago, IL, USA},
  dont_doi = {http://doi.acm.org/10.1145/1065010.1065015},
  dont_publisher = {ACM Press},
  dont_address = {New York, NY, USA},
}

@Article{abadi-lamport-TCS91,
  author = 	 {M. Abadi and L. Lamport},
  title = 	 {The existence of refinement mappings},
  journal = 	 {Theor. Comput. Sci.},
  year = 	 {1991},
  volume = 	 {82},
  number = 	 {2},
}

@InProceedings{tasiran-qadeer-RV04,
  author =       {S. Tasiran and S. Qadeer},
  title =        {Runtime refinement verification of concurrent data structures},
  booktitle = {Runtime Verification},
  year =      {2004},
  series =    {Electronic Notes in Theoretical Computer Science},
  dont_publisher = {Elsevier}
}

@Article{freund-qadeer-JOT04,
  author =       {S. Freund and S. Qadeer},
  title =        {Checking Concise Specifications for Multithreaded Software},
  journal =      {Journal of Object Technology},
  year =         {2004},
  volume =    {3},
  number =    {6},
  pages =     {81--101},
  url = {\url{http://www.jot.fm/issues/issue_2004_06/article4}},
  month =     {June}
}

@inproceedings{ranganathan-pai-adve-97,
 author = {P. Ranganathan and V. Pai and S. Adve},
 title = {Using speculative retirement and larger instruction windows to narrow the performance gap between memory consistency models},
 booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
 year = {1997},
 isbn = {0-89791-890-8},
 pages = {199--210},
 location = {Newport, Rhode Island, United States},
 doi = {http://doi.acm.org/10.1145/258492.258512},
 dont_publisher = {ACM Press},
 }

@article{hill-98,
 author = {M. Hill},
 title = {Multiprocessors Should Support Simple Memory-Consistency Models},
 journal = {Computer},
 volume = {31},
 number = {8},
 year = {1998},
 issn = {0018-9162},
 pages = {28--34},
 doi = {http://dx.doi.org/10.1109/2.707614},
 dont_publisher = {IEEE Computer Society Press},
 }

@article{sundell-tsigas-JPDC05,
 author = {H. Sundell and P. Tsigas},
 title = {Fast and lock-free concurrent priority queues for multi-thread systems},
 journal = {J. Parallel Distrib. Comput.},
 volume = {65},
 number = {5},
 year = {2005},
 issn = {0743-7315},
 pages = {609--627},
 doi = {http://dx.doi.org/10.1016/j.jpdc.2004.12.005},
 dont_publisher = {Academic Press, Inc.},
 address = {Orlando, FL, USA},
 }


@inproceedings{michael-scott-PODC96,
 author = {M. Michael and M. Scott},
 title = {Simple, fast, and practical non-blocking and blocking concurrent queue algorithms},
 booktitle = {Principles of Distributed Computing (PODC)},
 year = {1996},
 dont_isbn = {0-89791-800-2},
 pages = {267--275},
 dont_location = {Philadelphia, Pennsylvania, United States},
 dont_doi = {http://doi.acm.org/10.1145/248052.248106},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@article{fraser-harris-TACM07,
 author = {K. Fraser and T. Harris},
 title = {Concurrent programming without locks},
 journal = {ACM Trans. Comput. Syst.},
 volume = {25},
 number = {2},
 year = {2007},
 }

Concurrent programming without locks

@TechReport{michael-scott-TR-95,
  author =       {M. Michael and M. Scott},
  title =        {Correction of a Memory Management Method for Lock-Free Data Structures},
  institution =  {University of Rochester},
  year =         {1995},
  number =    {TR599},
}


@inproceedings{coons-musuvathi-burckhardt-PPoPP10,
 author = {K. Coons and M. Musuvathi and S. Burckhardt },
 title = {{Gambit}: Effective Unit Testing of Concurrency Libraries},
 booktitle = {Principles and Practice of Parallel Programming (PPoPP)},
 year = {2010},
}

@InProceedings{yang-gopalakrishnan-lindstrom-ICFEM04,
  author =       {Y. Yang and G. Gopalakrishnan and G. Lindstrom},
  title =        {Memory-Model-Sensitive Data Race Analysis},
  booktitle = {International Conference on Formal Engineering Methods (ICFEM)},
  pages =     {30--45},
  year =      {2004},
  dont_number =    {3308},
  series =    {LNCS 3308},
  publisher = {Springer},
}


@article{herlihy-TOPLAS91,
 author = {M. Herlihy},
 title = {Wait-free synchronization},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {13},
 number = {1},
 year = {1991},
 issn = {0164-0925},
 pages = {124--149},
 doi = {http://doi.acm.org/10.1145/114005.102808},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{peterson-TOPLAS83,
 author = {G. Peterson},
 title = {Concurrent Reading While Writing},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {5},
 number = {1},
 year = {1983},
 issn = {0164-0925},
 pages = {46--55},
 doi = {http://doi.acm.org/10.1145/357195.357198},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{lamport-CACM77,
 author = {L. Lamport},
 title = {Concurrent reading and writing},
 journal = {Commun. ACM},
 volume = {20},
 number = {11},
 year = {1977},
 issn = {0001-0782},
 pages = {806--811},
 doi = {http://doi.acm.org/10.1145/359863.359878},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{denning-dennis-CACM10,
 author = {P. Denning and J. Dennis},
 title = {The Resurgence of Parallelism},
 journal = {Commun. ACM},
 volume = {53},
 number = {6},
 year = {2010},
 }

@article{lamport-CACM77,
 author = {L. Lamport},
 title = {Concurrent reading and writing},
 journal = {Commun. ACM},
 volume = {20},
 number = {11},
 year = {1977},
 issn = {0001-0782},
 pages = {806--811},
 doi = {http://doi.acm.org/10.1145/359863.359878},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }




@article{shasha-snir-TOPLAS88,
 author = {D. Shasha and M. Snir},
 title = {Efficient and correct execution of parallel programs that share memory},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {10},
 number = {2},
 year = {1988},
 issn = {0164-0925},
 pages = {282--312},
 doi = {http://doi.acm.org/10.1145/42190.42277},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@inproceedings{fang-lee-midkiff-ICS03,
 author = {X. Fang and J. Lee and S. Midkiff},
 title = {Automatic fence insertion for shared memory multiprocessing},
 booktitle = {International Conference on Supercomputing (ICS)},
 year = {2003},
 dont_isbn = {1-58113-733-8},
 pages = {285--294},
 dont_location = {San Francisco, CA, USA},
 dont_doi = {http://doi.acm.org/10.1145/782814.782854},
 dont_publisher = {ACM},
 dont_address = {New York, NY, USA},
 }

@inproceedings{michael-PLDI04,
 author =    {M. Michael},
 title =     {Scalable lock-free dynamic memory allocation},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year =      {2004},
 isbn =      {1-58113-807-5},
 pages =     {35--46},
 dont_location =  {Washington DC, USA},
 dont_doi = {http://doi.acm.org/10.1145/996841.996848},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{burckhardt-alur-martin-CAV06,
  AUTHOR    = {S. Burckhardt and R. Alur and M. Martin},
  TITLE     = {Bounded Verification of Concurrent Data Types on Relaxed Memory Models: A Case Study},
  BOOKTITLE = {Computer-Aided Verification (CAV)},
  YEAR      = {2006},
  PAGES     = {489--502},
  PUBLISHER = {Springer},
  SERIES    = {LNCS 4144},
}

@inproceedings{farzan-madhusudan-CAV08,
  AUTHOR    = {A. Farzan and P. Madhusudan},
  TITLE     = {Monitoring Atomicity in Concurrent Programs},
  BOOKTITLE = {Computer-Aided Verification (CAV)},
  YEAR      = {2008}
}




@Manual{pfx-ctp,
  title =  {Parallel Extensions to the {.NET FX CTP}},
  organization = {MSDN},
  month =        {November},
  year =         {2007}, 
  address = {\url{http://blogs.msdn.com/somasegar/archive/2007/11/29/parallel-extensions-to-the-net-fx-ctp.aspx}}
}

@Manual{pfx-source,
  title =        {.NET Framework 4 Data Structures for Parallel Programming},
  organization = {MSDN},
  month =        {November},
  year =         {2009},
  address = {\url{http://msdn.microsoft.com/en-us/library/dd460718(VS.100).aspx}},
}



@inproceedings{vechev-yahav-yorsh-SPIN09,
  author    = {M. Vechev and
               E. Yahav and
               G. Yorsh},
  title     = {Experience with Model Checking Linearizability},
  booktitle = {SPIN},
  year      = {2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}




@inproceedings{burckhardt-alur-martin-PLDI07,
  author = {S. Burckhardt and R. Alur and M. Martin},
  title = {{CheckFence}: Checking Consistency of Concurrent Data Types on Relaxed Memory Models},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  pages = {12--21},
  year = {2007},
}

@inproceedings{colvin-groves-luchangco-moir-CAV06,
  AUTHOR    = {R. Colvin and L. Groves and V. Luchangco and M. Moir},
  TITLE     = {Formal Verification of a Lazy Concurrent List-Based Set Algorithm},
  BOOKTITLE = {Computer-Aided Verification (CAV)},
  YEAR      = {2006},
  PAGES     = {475--488},
  PUBLISHER = {Springer},
  SERIES    = {LNCS 4144},
}

@Misc{victor-info,
  author =    {V. Luchangco},
  title =     {Personal Communications},
  month =     {October},
  year =      {2006},
}

@inproceedings{gao-hesselink-CAV04,
  AUTHOR    = {H. Gao and W. Hesslink},
  TITLE     = {A Formal Reduction for Lock-Free Parallel Algorithms},
  BOOKTITLE = {Computer-Aided Verification (CAV)},
  YEAR      = {2004},
  PAGES     = {44--56},
  PUBLISHER = {Springer},
  SERIES    = {LNCS 3114},
}

@article{herlihy-TOPLAS93,
 author = {M. Herlihy},
 title = {A methodology for implementing highly concurrent data objects},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {15},
 number = {5},
 year = {1993},
 issn = {0164-0925},
 pages = {745--770},
 doi = {http://doi.acm.org/10.1145/161468.161469},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@inproceedings{owre-rushby-shankar-CADE92,
    AUTHOR = {{S.} Owre and {J.} Rushby and and {N.} Shankar},
    TITLE = {{PVS:} {A} Prototype Verification System},
    BOOKTITLE = {Conference on Automated Deduction (CADE)},
    YEAR = {1992},
    EDITOR = {Deepak Kapur},
    SERIES = {Lecture Notes in Artificial Intelligence},
    VOLUME = {607},
    PAGES = {748--752},
    ADDRESS = {Saratoga, {NY}},
    MONTH = {jun},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/cade92-pvs/}
}

@inproceedings{moir-PODC97,
 author = {M. Moir},
 title = {Practical implementations of non-blocking synchronization primitives},
 booktitle = {Principles of distributed computing (PODC)},
 year = {1997},
 isbn = {0-89791-952-1},
 pages = {219--228},
 dont_location = {Santa Barbara, California, United States},
 doi = {http://doi.acm.org/10.1145/259380.259442},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@inproceedings{lamport-DISC06,
 author = {L. Lamport},
 title = {Checking a Multithreaded Algorithm with \raisebox{.7mm}{+}{CAL}},
 booktitle = {Conference on Distributed Computing (DISC)},
 year = {2006},
 series =    {LNCS 4167},
 pages = {151--163},
 publisher = {Springer},
}

@inproceedings{harris-fraser-pratt-DISC02,
 author = {T. Harris and K. Fraser and I. Pratt},
 title = {A Practical Multi-word Compare-and-Swap Operation},
 booktitle = {Conference on Distributed Computing (DISC)},
 year = {2002},
 series =    {LNCS 2508},
 pages = {265--279},
 publisher = {Springer},
}

@inproceedings{harris-DISC01,
 author = {T. Harris},
 title = {A Pragmatic Implementation of Non-blocking Linked-Lists},
 booktitle = {Conference on Distributed Computing (DISC)},
 year = {2001},
 series =    {LNCS 2180},
 pages = {300--314},
 publisher = {Springer},
}

@inproceedings{detlefs-flood-et-al-DISC00,
 author = {D. Detlefs and C. Flood and A. Garthwaite and P. Martin and N. Shavit and G. Steele},
 title = {Even Better {DCAS}-Based Concurrent Deques},
 booktitle = {Conference on Distributed Computing (DISC)},
 year = {2000},
 series =    {LNCS 1914},
 pages = {59--73},
 publisher = {Springer},
}


@inproceedings{anderson-moir-PODC95,
 author = {J. H. Anderson and M. Moir},
 title = {Universal constructions for multi-object operations},
 booktitle = {Principles of Distributed Computing (PODC)},
 year = {1995},
 isbn = {0-89791-710-3},
 pages = {184--193},
 location = {Ottowa, Ontario, Canada},
 doi = {http://doi.acm.org/10.1145/224964.224985},
 publisher = {ACM Press},
 address = {New York, NY, USA},
}

@inproceedings{heller-et-al-OPODIS05,
  author = {S. Heller and M. Herlihy and V. Luchangco and M. Moir and W. Scherer and N. Shavit},
  title = {A Lazy Concurrent List-Based Set Algorithm},
  booktitle = {Principles of Distributed Systems (OPODIS)},
  year = {2005}
}


@PhdThesis{gharacharloo-dissertation,
  author =       {K. Gharachorloo},
  title =        {Memory Consistency Models for Shared-Memory Multiprocessors},
  school =       {University of Utah},
  year =         {2005},
  OPTkey =       {},
  OPTtype =      {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}


@PhdThesis{yang-dissertation,
  author =       {Jason Yue Yang},
  title =        {Formalizing Shared Memory Consistency Models for Program Analysis},
  school =       {University of Utah},
  year =         {2005},
  OPTkey =       {},
  OPTtype =      {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}



@PhdThesis{fraser-dissertation,
  author =       {Keir Fraser},
  title =        {Practical Lock-Freedom},
  school =       {University of Cambridge},
  year =         {2004},
  OPTkey =       {},
  OPTtype =      {},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@Misc{ fraser-lock-free-lib,
  author =    {K. Fraser},
  title =     {lock-free-lib.tar.gz},
  howpublished = {\url{http://www.cl.cam.ac.uk/Research/SRG/netos/lock-free/}},
}


@InProceedings{vonpraun-cain-choi-ryu-ISCA06,
  author =    {C. von Praun and T. Cain and J. Choi and K. Ryu},
  title =     {Conditional Memory Ordering},
  booktitle = {International Symposium on Computer Architecture (ISCA)},
  dont_publisher = {ACM},
  year =      {2006},
}

@article{abadi-flanagan-freund-TOPLAS06,
 author = {M. Abadi and C. Flanagan and S. Freund},
 title = {Types for safe locking: Static race detection for {Java}},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {28},
 number = {2},
 year = {2006},
 issn = {0164-0925},
 pages = {207--255},
 doi = {http://doi.acm.org/10.1145/1119479.1119480},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@inproceedings{boyapati-lee-rinard-OOPSLA02,
 author = {C. Boyapati and R. Lee and M. Rinard},
 title = {Ownership types for safe programming: preventing data races and deadlocks},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2002},
 isbn = {1-58113-471-1},
 pages = {211--230},
 dont_location = {Seattle, Washington, USA},
 doi = {http://doi.acm.org/10.1145/582419.582440},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{burckhardt-leijen-yi-sadowski-ball-OOPSLA11,
 author = {S. Burckhardt and D. Leijen and J. Yi and C. Sadowski and T. Ball},
 title = {Two for the Price of One: A Model for Parallel and Incremental Computation (Distinguished Paper Award)},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2011},
}

@inproceedings{bocchino-et-al-OOPSLA09,
 author = {R. Bocchino and V. Adve and D. Dig. and S. Adve and S. Heumann and R. Komuravelli and J. Overbey and P. Simmons and H. Sung  and M. Vakilian },
 title = {A Type and Effect System for {Deterministic Parallel Java}},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2009},
}


@inproceedings{musuvathi-et-al-OSDI08,
  author    = {M. Musuvathi and
               S. Qadeer and
               T. Ball and
               G. Basler and
               P. Nainar and
               I. Neamtiu},
  title     = {Finding and Reproducing Heisenbugs in Concurrent Programs},
  booktitle = {Operating Systems Design and Impl. (OSDI)},
  year      = {2008},
  pages     = {267-280}
}

@inproceedings{musuvathi-qadeer-PLDI08,
  author    = {M. Musuvathi and S. Qadeer},
  title     = {Fair stateless model checking},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year      = {2008}
}

@inproceedings{henzinger-jhala-majumdar-PLDI04,
 author = {T. Henzinger and R. Jhala and R. Majumdar},
 title = {Race checking by context inference},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2004},
 isbn = {1-58113-807-5},
 pages = {1--13},
 dont_location = {Washington DC, USA},
 doi = {http://doi.acm.org/10.1145/996841.996844},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@inproceedings{naik-aiken-whaley-PLDI06,
 author = {M. Naik and A. Aiken and J. Whaley},
 title = {Effective static race detection for {Java}},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2006},
 isbn = {1-59593-320-4},
 pages = {308--319},
 dont_location = {Ottawa, Ontario, Canada},
 doi = {http://doi.acm.org/10.1145/1133981.1134018},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{boehm-PLDI05,
 author = {H.-J. Boehm},
 title = {Threads cannot be implemented as a library},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2005},
 isbn = {1-59593-056-6},
 pages = {261--268},
 dont_location = {Chicago, IL, USA},
 doi = {http://doi.acm.org/10.1145/1065010.1065042},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{manson-pugh-adve-POPL05,
 author = {J. Manson and W. Pugh and S. Adve},
 title = {The {Java} Memory Model},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2005},
 isbn = {1-58113-830-X},
 dont_pages = {378--391},
 dont_location = {Long Beach, California, USA},
 doi = {http://doi.acm.org/10.1145/1040305.1040336},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@InProceedings{blundell-lewis-martin-WDDD05,
  author = 	 {C. Blundell and E. Lewis and M. Martin},
  title = 	 {Deconstructing transactions: The subtleties of atomicity},
  year = 	 {2005},
  booktitle =    {Workshop on Duplicating, Deconstructing, and Debunking (WDDD)}
}

@InProceedings{burckhardt-leijen-fahndrich-wodet11,
  author = 	 {S. Burckhardt and D. Leijen and M. F\"ahndrich},
  title =  {Roll Forward, Not Back: A Case for Deterministic Conflict Resolution},
  booktitle = {Workshop on Determinism and Correctness in Parallel Programming},
  year =      {2011},
}

@InProceedings{grossman-manson-pugh-MSPC06,
  author = 	 {D. Grossman, J. Manson, W. Pugh},
  title = 	 {What do high-level memory models mean for transactions? },
  year = 	 {2006},
  booktitle =    {Workshop on memory system performance and correctness (MSPC)}
}
 
 
@InProceedings{lea-CSJP04,
  author =       {Doug Lea},
  title =        {The java.util.concurrent Synchronizer Framework},
  year =         {2004},
  booktitle =    {PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP)}
}

@InProceedings{yang-gopalakrishnan-lindstrom-CSJP04,
  author =       {Y. Yang and G. Gopalakrishnan and G. Lindstrom},
  title =        {Rigorous Concurrency Analysis of Multithreaded Programs},
  year =         {2004},
  booktitle =    {PODC Workshop on Concurrency and Synchronization in Java Programs (CSJP)}
}

@InProceedings{trachsel-praun-gross-IPDPS06,
  author =       {O. Trachsel and C. von Praun and T. Gross},
  title =        {On the Effectiveness of Speculative and Selective Memory Fences},
  booktitle =    {International Parallel and Distributed Processing Symposium (IPDPS)},
  year =         {2006},
}

@article{harris-et-al-MICRO07,
  author    = {T. Harris and
               A. Cristal and
               O. Unsal and
               E. Ayguad{\'e} and
               F. Gagliardi and
               B. Smith and
               M. Valero},
  title     = {Transactional Memory: An Overview},
  journal   = {IEEE Micro},
  volume    = {27},
  number    = {3},
  year      = {2007},
  pages     = {8-29},
  ee        = {http://doi.ieeecomputersociety.org/10.1109/MM.2007.63},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{devietti-lucia-ceze-oskin-IEEE10, 
author={J. Devietti and B. Lucia and L. Ceze and M. Oskin}, 
journal={Micro, IEEE}, title={{DMP}: Deterministic Shared-Memory Multiprocessing}, 
year={2010}, 
_month={jan.-feb. }, 
volume={30}, 
number={1}, 
pages={40 -49}, 
keywords={}, 
doi={10.1109/MM.2010.14}, 
ISSN={0272-1732},}


@InProceedings{bergan-anderson-devietti-ceze-grossman-ASPLOS10,
  author = 	 {T. Bergan and O. Anderson and J. Devietti and L. Ceze and D. Grossman},
  title = 	 {{CoreDet}: A Compiler and Runtime System for Deterministic Multithreaded Execution},
  booktitle = {Architectural Support for Programming Languages and Operating Systems (ASPLOS)},
  year = 	 {2010},
}

@InProceedings{jacobs-smans-piessens-schulte-TV06,
  author =       {B. Jacobs and J. Smans and F. Piessens and W. Schulte},
  title =        {A Simple Sequential Reasoning Approach for Sound Modular Verification of Mainstream Multithreaded Programs},
  booktitle =    {TV'06 Workshop, Federated Logic Conference (FLoC)},
  pages =        {66--77},
  year =         {2006},
}

@inproceedings{vonpraun-gross-OOPSLA01,
 author = {C. von Praun and T. Gross},
 title = {Object race detection},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2001},
 isbn = {1-58113-335-9},
 pages = {70--82},
 dont_location = {Tampa Bay, FL, USA},
 doi = {http://doi.acm.org/10.1145/504282.504288},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{berger-yang-liu-novark-OOPSLA09,
 author = {E. Berger and T. Yang and T. Liu and G. Novark},
 title = {Grace: Safe Multithreaded Programming for {C/C++}},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2009},
}

@inproceedings{pratikakis-foster-hicks-PLDI06,
 author = {P. Pratikakis and J. Foster and M. Hicks},
 title = {{LOCKSMITH}: context-sensitive correlation analysis for race detection},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2006},
 isbn = {1-59593-320-4},
 pages = {320--331},
 dont_location = {Ottawa, Ontario, Canada},
 doi = {http://doi.acm.org/10.1145/1133981.1134019},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{flanagan-freund-PLDI2000,
 author = {C. Flanagan and S. Freund},
 title = {Type-based race detection for {Java}},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2000},
 isbn = {1-58113-199-2},
 pages = {219--232},
 dont_location = {Vancouver, British Columbia, Canada},
 doi = {http://doi.acm.org/10.1145/349299.349328},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{flanagan-freund-PLDI09,
 author = {C. Flanagan and S. Freund},
 title = {Efficient and Precise Dynamic Race Detection},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2009},
}

@inproceedings{marino-musuvathi-narayanasamy-PDLI09,
 author = {D. Marino and M. Musuvathi and S. Narayanasamy},
 title = {{LiteRace}: Effective Sampling for Lightweight Data-Race Detection},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2009},
}

@InProceedings{huynh-roychoudhury-FM06,
  author =       {T. Huynh and A. Roychoudhury},
  title =        {A Memory Model Sensitive Checker for {C\#}},
  booktitle = {Formal Methods (FM)},
  pages =     {476--491},
  year =      {2006},
  series =    {LNCS 4085},
  publisher = {Springer},
}

@Misc{ burckhardt-homepage,
  author =    {S. Burckhardt},
  title =     {{CheckFence}},
  howpublished = {\url{http://www.cis.upenn.edu/$\sim$sburckha/checkfence/}},
}

@inproceedings{attiya-welch-SPAA91,
 author = {H. Attiya and J. Welch},
 title = {Sequential consistency versus linearizability (extended abstract)},
 booktitle = {Symposium on Parallel Algorithms and Architectures (SPAA)},
 year = {1991},
 isbn = {0-89791-438-4},
 pages = {304--315},
 location = {Hilton Head, South Carolina, United States},
 doi = {http://doi.acm.org/10.1145/113379.113407},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }



@techreport{ detlefs-leino-nelson-saxe-TR98,
    author = {D. Detlefs and R. Leino and G. Nelson and J. Saxe},
    institution = {Compaq Systems Research Center},
    title = {Extended Static Checking},
    number = {159},
    year = {1998},
}

@techreport{ leino-saxe-stata-TR99,
    author = {R. Leino and J. Saxe and R. Stata},
    institution = {Compaq Systems Research Center},
    title = {Checking java programs via guarded commands},
    number = {1999-002},
    year = {1999},
}

@inproceedings{ jackson-vaziri-ISSTA00,
 author = {D. Jackson and M. Vaziri},
 title = {Finding bugs with a constraint solver},
 booktitle = {International Symposium on Software Testing and Analysis},
 year = {2000},
 cont_isbn = {1-58113-266-2},
 pages = {14--25},
 cont_location = {Portland, Oregon, United States},
 doi = {http://doi.acm.org/10.1145/347324.383378},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
 }

@inproceedings{leroy-POPL06,
 author = {X. Leroy},
 title = {Formal certification of a compiler back-end},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2006},
 dont_isbn = {1-59593-027-2},
 pages = {42--54},
 dont_location = {Charleston, South Carolina, USA},
 dont_doi = {http://doi.acm.org/10.1145/1111037.1111042},
 dont_publisher = {ACM Press},
 dont_address = {New York, NY, USA},
}

@inproceedings{elmas-qadeer-tasiran-POPL09,
 author = {T. Elmas and S. Qadeer and S. Tasiran},
 title = {A calculus of atomic actions},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2009},
 }

@inproceedings{blazy-dargaye-leroy-FM06,
  author    = {S. Blazy and Z. Dargaye and X. Leroy},
  title     = {Formal Verification of a C Compiler Front-End},
  booktitle = {Formal Methods (FM)},
  year      = {2006},
  pages     = {460--475},
  series =    {LNCS 4085},
  publisher = {Springer},
  dont_ee        = {http://dx.doi.org/10.1007/11813040_31},
  dont_bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{musuvathi-qadeer-PLDI07,
  author    = {M. Musuvathi and
               S. Qadeer},
  title     = {Iterative context bounding for systematic testing of multithreaded
               programs.},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year      = {2007},
  pages     = {446-455},
  ee        = {http://doi.acm.org/10.1145/1250734.1250785}
}



@article{lamport-CACM74,
  author    = {L. Lamport},
  title     = {A New Solution of Dijkstra's Concurrent Programming Problem},
  journal   = {Communications of the ACM},
  volume    = {17},
  number    = {8},
  year      = {1974},
  pages     = {453-455}
}

@book{benari-PCP82,
   author = {M. Ben-Ari},
   title = {Principles of Concurrent Programming},
   year = {1982},
   isbn = {0137010788},
   publisher = {Prentice Hall Professional Technical Reference},
 }

@inproceedings{verisoft,
   author = "P. Godefroid",
   title = "Model Checking for Programming Languages using {V}eriSoft",
   booktitle = "Principles of Programming Languages (POPL)", 
   pages = "174--186", 
   year = "1997"
} 

@book{godefroid96partial,
   author = {P. Godefroid},
   title = {Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem},
   year = {1996},
   series = "LNCS 1032",
   publisher = {Springer Verlag}
 }

@inproceedings{flanagan-godefroid-POPL05,
   author = "C. Flanagan and P. Godefroid", 
   title = "Dynamic partial-order reduction for model checking software",
   booktitle = "Principles of Programming Languages (POPL)",
   year = "2005"
}

@article{hill-ieee-98,
  author    = {M. Hill},
  title     = {Multiprocessors Should Support Simple Memory-Consistency
               Models},
  journal   = {IEEE Computer},
  volume    = {31},
  number    = {8},
  year      = {1998},
  pages     = {28-34}
}

@TechReport{burckhardt-musuvathi-sober08,
  author = 	{S. Burckhardt and M. Musuvathi},
  title = 	"Effective program verification for relaxed memory models",
  institution = "Microsoft Research",		  
  year = 	2008,
  number = {MSR-TR-2008-12}
}

@InProceedings{gibbons-korach-PDPS92,
  author =       {P. B. Gibbons and E. Korach},
  title =        {The complexity of sequential consistency},
  booktitle = {Parallel and Distributed Processing},
  pages =     {317--325},
  year =      {1992},
  publisher = {IEEE}
}

@Misc{ jdblog,
  author =    {J. Duffy},
  title =     {{Joe Duffy's Weblog}},
  howpublished = {\url{http://www.bluebytesoftware.com/blog/2007/11/10/CLR20MemoryModel.aspx}},
}

@Misc{ cbblog,
  author =    {C. Brumme},
  title =     {cbrumme's WebLog},
  howpublished = {\url{http://blogs.gotdotnet.com/cbrumme/archive/2003/05/17/51445.aspx}},
}

@inproceedings{lerner-millstein-chambers,
 author = {Sorin Lerner and Todd Millstein and Craig Chambers},
 title = {Automatically proving the correctness of compiler optimizations},
 booktitle = {Programming Language Design and Impl. (PLDI)},
 year = {2003},
 pages     = {220-231}
}

@inproceedings{boehm-adve-PLDI08,
  author    = {Hans-Juergen Boehm and
               Sarita V. Adve},
  title     = {Foundations of the {C++} concurrency memory model},
  booktitle = {Programming Language Design and Impl. (PLDI)},
  year      = {2008},
  pages     = {68-78}
}

@article{young-jar,
 author = {William D. Young},
 title = {A mechanically verified code generator},
 journal = {Journal of Automated Reasoning},
 volume = {5},
 number = {4},
 year = {1989},
 issn = {0168-7433},
 pages = {493--518}
 }

@article{klein-nipkow,
 author = {Gerwin Klein and Tobias Nipkow},
 title = {A machine-checked model for a Java-like language, virtual machine, and compiler},
 journal = {ACM Transactions on Programming Languages and Systems},
 volume = {28},
 number = {4},
 year = {2006},
 pages = {619--695}
 }

@inproceedings{leroy-popl,
 author = {Xavier Leroy},
 title = {Formal certification of a compiler back-end or: programming a compiler with a proof assistant},
 booktitle = {Principles of programming languages (POPL)},
 year = {2006},
 pages = {42--54}
 }

@inproceedings{sevcik-ecoop08,
 author = {J. Sevcik and D. Aspinall},
 title = {On Validity of Program Transformations in the {J}ava Memory Model},
 booktitle = {European Conference on Object-Oriented Programming (ECOOP)},
 year = {2008},
 }

@inproceedings{z3,
  author    = {Leonardo Mendon\c{c}a de Moura and
               Nikolaj Bj{\o}rner},
  title     = {Z3: An Efficient SMT Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of
               Systems},
  year      = {2008},
  pages     = {337-340}
}


@Misc{ doug-lea-cookbook,
  author =    {Doug Lea},
  title =     {The JSR-133 Cookbook for Compiler Writers},
  howpublished = {\url{http://gee.cs.oswego.edu/dl/jmm/cookbook.html}},
}


@TechReport{traver-techreport,
  author = 	{S. Burckhardt and M. Musuvathi and V. Singh},
  title = 	"Verification of compiler transformations for concurrent programs",
  institution = "Microsoft Research",		  
  year = 	2008,
  number = {MSR-TR-2008-171}
}

@inproceedings{saraswat-rao,
 author = {V. Saraswat and R. Jagadeesan and M. Michael and C. von Praun},
 title = {A theory of memory models},
 booktitle = {PPoPP '07: Principles and practice of parallel programming},
 year = {2007},
 pages = {161--172}
 }

@INPROCEEDINGS{cenciarelli07,
    author = {P. Cenciarelli and E. Sibilio},
    title = {The Java memory model: Operationally, denotationally, axiomatically},
    booktitle = {In 16th European Symposium on Programming (ESOP)},
    year = {2007} }

@article{shasha-snir-TOPLAS88,
 author = {D. Shasha and M. Snir},
 title = {Efficient and correct execution of parallel programs that share memory},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {10},
 number = {2},
 year = {1988},
 issn = {0164-0925},
 pages = {282--312},
 doi = {http://doi.acm.org/10.1145/42190.42277},
 dont_publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@inproceedings{burckhardt-musuvathi-CAV08, 
  author = {S. Burckhardt and M. Musuvathi}, 
  title = {Effective Program Verification for Relaxed Memory Models}, 
  booktitle = {Computer-Aided Verification (CAV)}, 
  pages = {107--120}, 
  year = {2008}, 
} 


@TechReport{sewell-tr,
  author =       {S. Owens and S. Sarkar and P. Sewell},
  title =        {A Better x86 Memory Model: {x86-TSO} (Extended Version)},
  institution =  {Univ. of Cambridge},
  year =         {2009},
  OPTkey =       {},
  OPTtype =      {},
  number =    {UCAM-CL-TR-745},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@inproceedings{sarkar-sewell-et-al-POPL09,
 author = {S. Sarkar et al.},
 title = {The Semantics of {x86-CC} Multiprocessor Machine Code},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2009},
}

@inproceedings{boudol-petri-POPL09,
 author = {G. Boudol and G. Petri},
 title = {Relaxed memory models: an operational approach},
 booktitle = {Principles of Programming Languages (POPL)},
 year = {2009},
}



@inproceedings{brooks-LICS93,
  author    = {S. Brookes},
  title     = {Full Abstraction for a Shared Variable Parallel Language},
  booktitle = {LICS},
  year      = {1993},
  pages     = {98-109},
}

@inproceedings{arvind-maessen-ISCA06,
  author    = {Arvind and J.-W. Maessen},
  title     = {Memory Model = Instruction Reordering + Store Atomicity},
  booktitle = {ISCA},
  year      = {2006},
  pages     = {29-40},
}

@inproceedings{shen-arvind-rudolph-ISCA99,
  author    = {X. Shen and
               Arvind and
               L. Rudolph},
  title     = {Commit-Reconcile {\&} Fences (CRF): A New Memory Model
               for Architects and Compiler Writers},
  booktitle = {ISCA},
  year      = {1999},
  pages     = {150-161},
}

@PhdThesis{sevcik-dissertation,
  author = 	 {J. Sevcik},
  title = 	 {Program Transformations in Weak Memory Models},
  school = 	 {University of Edinburgh},
  year = 	 {2008},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

%--------- DAAN ----------

@INPROCEEDINGS{Jagannathan:safefutures,
 author = {A. Welc and S. Jagannathan and A. Hosking},
 title = {Safe futures for Java},
 booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
 year = {2005},
 pages = {439--453},
}

@ARTICLE{Hicks:safefutures,
 author = {P. Pratikakis and J. Spacco and M. Hicks},
 title = {Transparent proxies for java futures},
 journal = {SIGPLAN Not.},
 volume = {39},
 number = {10},
 year = {2004},
 issn = {0362-1340},
 pages = {206--223}
}

@INPROCEEDINGS{Steele:parfortress,
  author = {G. Steele},
  title  = {Parallel Programming and Parallel Abstractions in Fortress},
  booktitle = {Invited talk at the Eighth International Symposium on Functional and Logic Programming ({FLOPS})},
  month   = apr,
  year    = 2006,
}



@UNPUBLISHED{ms:pex,
  author = {Microsoft},
  title = {Parallel Programming Samples, {.NET} Framework 4},
  year  = 2010,
  month = May,
  note = {\url{http://code.msdn.microsoft.com/ParExtSamples}}
}

@INPROCEEDINGS{Leijen:tpl,
  author = {D. Leijen and W. Schulte and S. Burckhardt},
  title = {The Design of a Task Parallel Library},
  booktitle = {Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)},
  year = 2009
}

@INPROCEEDINGS{Moreau:futuresemantics,
    author = {L. Moreau},
    title = {The semantics of Scheme with future},
    booktitle = {In In ACM SIGPLAN International Conference on Functional Programming (ICFP'96},
    year = {1996},
    pages = {146--156}
}

@INPROCEEDINGS{Flanagan:futuresemantics,
    author = {C. Flanagan and M. Felleisen},
    title = {The Semantics of Future and Its Use in Program Optimization},
    booktitle = {Rice University},
    year = {1995},
    pages = {209--220}
}

@inproceedings{pH,
    author = "S. Aditya and Arvind and L. Augustsson and J.-W. Maessen and R. Nikhil",
    title = "{S}emantics of p{H}: {A} {P}arallel {D}ialect of {H}askell",
    booktitle = "Proc. Haskell Workshop, La Jolla, {CA} {USA}",
    month = "June",
    editor = "Hudak, Paul",
    pages = "35-49",
    year = "1995"
}

@inproceedings{fortress,
 author={E. Allen and D. Chase and C. Flood and V. Luchangco and J.-W. Maessen and S. Ryu and G. Steele Jr.},
 title ={Project Fortress: A Multicore Language for Multicore Processors},
 booktitle={Linux Magazine}, 
 month=sep,
 year=2007}


@Article{Danaher:JCilkExceptions,
author = {J.  Danaher and I. Lee and C. Leiserson},
title = {Programming with Exceptions in JCilk},
journal = {Science of Computer Programming (SCP)},
year = {2006},
month = dec,
publisher = {Elsevier},
volume = {63},
number = {2},
pages = {147--171}
} 

@InProceedings{Danaher:JCilk,
author = {J.  Danaher and I. Lee and C. Leiserson},
title = {The JCilk Language for Multithreaded Computing},
booktitle = {Synchronization and Concurrency in Object-Oriented Languages (SCOOL)},
year = {2005},
month = oct,
address = {San Diego, California}
} 

@InProceedings{Frigo:Cilk,
author = {M. Frigo and C. Leiserson and K. Randall},
title = {The Implementation of the {C}ilk-5 Multithreaded Language},
booktitle = {Programming Language Design and Impl. {(PLDI)}},
year = {1998},
pages = {212--223}
} 

@InProceedings{ansel-et-al-PLDI09,
  title     = {{PetaBricks}: A Language and Compiler for Algorithmic Choice},
  author    = {J. Ansel and C. Chan and Y. Wong and M. Olszewski and Q. Zhao and A. Edelman and S. Amarasinghe},
  booktitle = pldi,
  year      = {2009},
}

@PhDThesis{Randall:Cilk,
author = {K. Randall},
title = {Cilk: Efficient Multithreaded Computing},
school = {Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology},
month = may,
year = {1998}
} 

@article{Blelloch:nesl,
        author = "G. Blelloch and S. Chatterjee and J. Hardwick and J. Sipelstein and M. Zagha",
        title = "Implementation of a Portable Nested Data-Parallel Language",
       	journal = "Journal of Parallel and Distributed Computing",
	volume = 21,
	number = 1,
        pages = "4--14",
	month = apr,
	year = 1994}

@inproceedings{Lea:forkjoin,
    author = "D. Lea",
    title = "A Java fork/join framework",
    booktitle = "Java Grande",
    pages = "36-43",
    year = "2000"}

@article{Acar:SelfAdjustingExperiments,
 author = {Acar, Umut A. and Blelloch, Guy E. and Blume, Matthias and Harper, Robert and Tangwongsan, Kanat},
 title = {An experimental analysis of self-adjusting computation},
 journal = toplas,
 volume = {32},
 issue = {1},
 month = {November},
 year = {2009},
 pages = {3:1--3:53},
}


@inproceedings{Acar:SelfAdjustingOverview,
 author = {Acar, Umut A.},
 title = {Self-adjusting computation (an overview)},
 booktitle = pepm,
 year = {2009},
}

@inproceedings{Hammer:ParallelSelfAdjusting,
 author = {Hammer, Matthew and Acar, Umut A. and Rajagopalan, Mohan and Ghuloum, Anwar},
 title = {A proposal for parallel self-adjusting computation},
 booktitle = {{Workshop on Declarative Aspects of Multicore Programming (DAMP)}},
 year = {2007},
  
}

@inproceedings{Guo:IncPy,
  title = {Towards Practical Incremental Recomputation for Scientists: An Implementation for the {Python} Language},
  booktitle = {Workshop on the Theory and Practice of Provenance (TAPP)},
  author = {Guo, Philip J. and Engler, Dawson},
  year = {2010},
}

@techreport{Acar:AdaptiveMemoization,
  author = {Acar, Umut A. and Blelloch, Guy E. and Harper, Robert},
  title = {Adaptive Memoization}, 
  institution = {Carnegie Mellon University}, 
  number = {CMU-CS-03-208},
  year = 2004,
}

@inproceedings{Hammer:Ceal09, 
  author = {Hammer, Matthew A. and Acar, Umut A. and Chen, Yan},
  title = {{CEAL}: a {C}-based language for self-adjusting computation},
  booktitle = pldi,
  year = 2009,
}

@inproceedings{Acar:SelfAdjustingTypes10,
  author = {Acar, Umut A. and Blelloch, Guy and Ley-Wild, Ruy and Tangwongsan, Kanat and T\"{u}rko\u{g}lu, Duru},
  title = {Traceable data types for self-adjusting computation},
  booktitle = pldi,
  year = 2010,
}

@inproceedings{Yellin:Inc91,
  author = {Yellin, Daniel M. and Strom, Robert E.},
  title = {{INC}: a language for incremental computations},
  booktitle = toplas,
  volume = 13,
  issue = 2,
  pages = {211 -- 236},
  year = 1991,
}

@inproceedings{Pugh:Inc89,
  author = {Pugh, William and Teitelbaum, Tim},
  title = {Incremental Computation via Function Caching},  
  booktitle = popl,
  year = 1989,
}

@inproceedings{Sundaresh:Inc91,
  author = {Sundaresh, R. S. and Hudak, Paul},
  title = {Incremental Computation via Partial Evaluation},
  booktitle = popl,
  year = 1991,
}

@inproceedings{Demers:Inc81,
 author = {Demers, Alan and Reps, Thomas and Teitelbaum, Tim},
 title = {Incremental evaluation for attribute grammars with application to syntax-directed editors},
 booktitle = popl,
 year = {1981},
}

@inproceedings{Reps:Inc82,
  author    = {Thomas W. Reps},
  title     = {Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors},
  booktitle = popl,
  year      = {1982},
}

@phdthesis{Hoover:Inc87,
 author = {Hoover, Roger},
 title = {Incremental graph evaluation},
 year = {1987},
 school = {Cornell University},
}

@inproceedings{Abadi:Inc96,
  author    = {Mart\'{\i}n Abadi and
               Butler W. Lampson and
               Jean-Jacques L{\'e}vy},
  title     = {Analysis and Caching of Dependencies},
  booktitle =icfp,
  year      = {1996},
}

@article{Liu:Inc98,
 author = {Liu, Yanhong A. and Stoller, Scott D. and Teitelbaum, Tim},
 title = {Static caching for incremental computation},
 journal = toplas,
 volume = {20},
 issue = {3},
 year = {1998},
 pages = {546--585},
}

@inproceedings{Heydon:Inc00,
 author = {Heydon, Allan and Levin, Roy and Yu, Yuan},
 title = {Caching function calls using precise dependencies},
 booktitle = pldi,
 year = {2000},
}

@inproceedings{Acar:Inc03,
 author = {Acar, Umut A. and Blelloch, Guy E. and Harper, Robert},
 title = {Selective memoization},
 booktitle =popl,
 year = {2003},
}

@inproceedings{Field:Inc90,
 author = {Field, John and Teitelbaum, Tim},
 title = {Incremental reduction in the lambda calculus},
 booktitle = {Conference on LISP and Functional Programming},
 year = {1990},
}


@phdthesis{Field:Inc91,
 author = {Field, John},
 title = {Incremental reduction in the lambda calculus and related reduction systems},
 year = {1991},
 school = {Cornell University},
}


@inproceedings{Ramalingam:Inc93,
 author = {Ramalingam, G. and Reps, Thomas},
 title = {A categorized bibliography on incremental computation},
 booktitle = popl,
 year = {1993},
}

@inproceedings{Shankar:Inc07,
 author = {Shankar, Ajeet and Bod\'{\i}k, Rastislav},
 title = {DITTO: automatic incrementalization of data structure invariant checks (in {Java})},
 booktitle = {Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation},
 year = {2007},
}

@inproceedings{Carlsson:Inc02,
 author = {Carlsson, Magnus},
 title = {Monads for incremental computing},
 booktitle = icfp,
 year = {2002},
}


@article{Acar:Lib06,
 author = {Acar, Umut and Blelloch, Guy and Blume, Matthias and Harper, Robert and Tangwongsan, Kanat},
 title = {A Library for Self-Adjusting Computation},
 journal = {Electronic Notes in Theoretical Computer Science},
 volume = {148},
 issue = {2},
 year = {2006},
 pages = {127--154},
}


@article{Olszewski:2009:KED:1508284.1508256,
 author = {Olszewski, Marek and Ansel, Jason and Amarasinghe, Saman},
 title = {Kendo: efficient deterministic multithreading in software},
 journal = {SIGPLAN Notices},
 volume = {44},
 issue = {3},
 _month = {March},
 year = {2009},
 issn = {0362-1340},
 pages = {97--108},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1508284.1508256},
 doi = {http://doi.acm.org/10.1145/1508284.1508256},
 acmid = {1508256},
 publisher = {ACM},
 _address = {New York, NY, USA},
 keywords = {debugging, determinism, deterministic multithreading, multicore, parallel programming},
}

@article{levenstein,
 author = {Navarro, Gonzalo},
 title = {A guided tour to approximate string matching},
 journal = {ACM Computing Surveys},
 volume = {33},
 issue = {1},
 _month = {March},
 year = {2001},
 issn = {0360-0300},
 pages = {31--88},
 numpages = {58},
 url = {http://doi.acm.org/10.1145/375360.375365},
 doi = {http://doi.acm.org/10.1145/375360.375365},
 acmid = {375365},
 _publisher = {ACM},
 _address = {New York, NY, USA},
 keywords = {Levenshtein distance, edit distance, online string matching, text searching allowing errors},
}


@inproceedings{AcarCoHuTu11pd,
 author =       "Umut A. Acar and Andrew Cotter and Beno{\^i}t Hudson
and  Duru T{\"u}rko{\u{g}}lu",
 title =        "Parallelism in Dynamic Well-Spaced Point Sets",
 booktitle =    "Proceedings of the 23rd ACM Symposium on Parallelism
in Algorithms and Architectures",
 year =         "2011",
 note =         "Symposium on Parallelism in Algorithms and Architectures",
}

@inproceedings{SumerAcIhMe11,
author = "Ozgur Sumer and Umut A. Acar and Alexander Ihler and Ramgopal Mettu", title = "Fast Parallel and Adaptive Updates for Dual-Decomposition Solvers", booktitle = "Conference on Artificial Intelligence (AAAI)", year = 2011 }

@inproceedings{BhatotiaWiRoAcPa11,
 author =       "Pramod Bhatotia  and Alexander Wieder and Rodrigo
Rodrigues and Umut A. Acar and Rafael Pasquini",
 title =        "Incoop: MapReduce for Incremental Computations",
 booktitle =    "ACM Symposium on Cloud Computing",
 year =         "2011"
}

@inproceedings{BhatotiaWiAkRoAc11,
 author =       "Pramod Bhatotia and Alexander Wieder and Istemi Ekin
Akkus and Rodrigo Rodrigues and Umut A. Acar",
 title =        "Large-scale Incremental Data Processing with Change
Propagation",
 booktitle =         "USENIX Workshop on Hot Topics in Cloud
Computing (HotCloud)",
 year =         "2011"
}

@inproceedings{yi-sadowski-flanagan-PPoPP11,
  author    = {J. Yi and
               C. Sadowski and
               C. Flanagan},
  title     = {Cooperative reasoning for preemptive execution},
  booktitle = {PPoPP},
  year      = {2011},
  pages     = {147-156},
  ee        = {http://doi.acm.org/10.1145/1941553.1941575},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@INPROCEEDINGS{kaplan-95,
    author = {H. Kaplan},
    title = {Persistent data structures},
    booktitle = {Handbook on Data Structures and Applications},
    year = {1995},
    pages = {241--246},
    publisher = {CRC Press}
}

@incollection{shapiro-kemme-09,
  author    = {M. Shapiro and
               B. Kemme},
  title     = {Eventual Consistency},
  booktitle = {Encyclopedia of Database Systems},
  year      = {2009},
  pages     = {1071-1072},
  ee        = {http://dx.doi.org/10.1007/978-0-387-39940-9_1366},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{gilbert-lynch-SIGACT02,
 author = {Gilbert, S. and Lynch, N.},
 title = {Brewer's conjecture and the feasibility of consistent, available, partition-tolerant web services},
 journal = {SIGACT News},
 volume = {33},
 issue = {2},
 month = {June},
 year = {2002},
 issn = {0163-5700},
 pages = {51--59},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/564585.564601},
 doi = {http://doi.acm.org/10.1145/564585.564601},
 acmid = {564601},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@article{terry-et-al-SIGOPS95,
 author = {Terry, D.  and Theimer, M.  and Petersen, K. and Demers, A.  and Spreitzer, M. and Hauser, C.},
 title = {Managing update conflicts in Bayou, a weakly connected replicated storage system},
 journal = {SIGOPS Oper. Syst. Rev.},
 volume = {29},
 issue = {5},
 month = {December},
 year = {1995},
 issn = {0163-5980},
 pages = {172--182},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/224057.224070},
 doi = {http://doi.acm.org/10.1145/224057.224070},
 acmid = {224070},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

@article{saito-shapiro-ACM05,
author = {Y. Saito and M. Shapiro},
title = {Optimistic replication},
journal = {ACM Computing Surveys},
volume = {37},
year = {2005},
pages = {42--81},
issue = {1},
doi = {10.1145/1057977.1057980},
masid = {1243097}
}

@inproceedings{decandia-et-al-SOSP07,
author = {G. Decandia and D. Hastorun and M. Jampani and G. Kakulapati and A. Lakshman and A. Pilchin and S. Sivasubramanian and P. Vosshall and W. Vogels},
title = {Dynamo: amazon's highly available key-value store},
booktitle = {Symposium on Operating Systems Principles},
year = {2007},
pages = {205--220},
doi = {10.1145/1294261.1294281},
masid = {4117687}
}

@inproceedings{valdes-tarjan-lawler-ACM79,
author = {J. Valdes and R. Tarjan and E. Lawler},
title = {The recognition of Series Parallel digraphs},
booktitle = {ACM Symposium on Theory of Computing},
year = {1979},
pages = {1--12},
doi = {10.1145/800135.804393},
masid = {576231}
}

@article{gray-et-al-sigmod96,
author = {J. Gray and P. Helland and P. O'Neil and D. Shasha},
title = {The Dangers of Replication and a Solution},
journal = {Sigmod Record},
volume = {25},
year = {1996},
pages = {173--182},
issue = {2},
doi = {10.1145/233269.233330},
masid = {667629}
}

@inproceedings{sun-ellis-CCSCW98,
author = {C. Sun and C. Ellis},
title = {Operational transformation in real-time group editors: issues, algorithms, and achievements},
booktitle = {Conference on Computer Supported Cooperative Work},
year = {1998},
pages = {59--68},
doi = {10.1145/289444.289469},
masid = {359491}
}

@article{imine-et-al-TCS06,
author = {A. Imine and M. Rusinowitch and G. Oster and P. Molli},
title = {Formal design and verification of operational transformation algorithms for copies convergence},
journal = {Theoretical Computer Science},
volume = {351},
year = {2006},
pages = {167--183},
issue = {2},
doi = {10.1016/j.tcs.2005.09.066},
masid = {1708062}
}

@article{shapiro-et-al-11,
author = {M. Shapiro and N. Preguia and C. Baquero and M. Zawirski},
title = {Conflict-free Replicated Data Types},
year = {2011},
masid = {48871078}
}

@article{petersen-et-al-OSR97,
author = {K. Petersen and M. Spreitzer and D. Terry and M. Theimer and A. Demers},
title = {Flexible Update Propagation for Weakly Consistent Replication},
journal = {Operating Systems Review},
volume = {31},
year = {1997},
pages = {288--301},
issue = {5},
doi = {10.1145/268998.266711},
masid = {66652}
}

@inproceedings{embedded-cc-sac-oops-2010,
 author = {F\"{a}hndrich, M{.} and Barnett, M{.} and Logozzo, F{.}},
 title = {Embedded {C}ontract {L}anguages},
 booktitle = {ACM Symposium on Applied Computing},
 year = 2010,
 }

@inproceedings{CousotCousot77,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Abstract interpretation: a unified lattice model for static 
                analysis of programs by construction or approximation of 
                fixpoints},
   year = 1977,
   booktitle = {ACM POPL},
}

@inproceedings{subpolyhedra,
 author = {Laviron, V{.} and Logozzo, F{.}},
 title = {SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities},
 booktitle = {VMCAI},
 year = {2009},
 }

@misc{codecontracts,
  author = 	 {F\"ahndrich, M{.} and  Barnett, M{.} and  Logozzo, F{.}},
  title = 	 {{CodeContract Tools}},
  url = "http://research.microsoft.com/contracts",
  month = 	 mar,
  year = 	 {2009} 
}

@inproceedings{cccheck,
  author    = {F{\"a}hndrich, M{.} and
               Logozzo, F{.}},
  title     = {Static Contract Checking with Abstract Interpretation},
  booktitle = {FoVeOOS},
  year      = {2010},
  pages     = {10-30}
}

@inproceedings{CousotCousotLogozzo-VMCAI11,
  author    = {Cousot, P{.} and
                Cousot, R{.} and
               Logozzo, F{.}},
  title     = {Precondition Inference from Intermittent Assertions and
               Application to Contracts on Collections},
  booktitle = {VMCAI},
  year      = {2011},
  pages     = {150-168}
}

@inproceedings{CousotCousotLogozzo-POPL11,
  author    = {Cousot, P{.} and
                Cousot, R{.} and
               Logozzo, F{.}},
  title     = {A parametric segmentation functor for fully automatic and
               scalable array content analysis},
  booktitle = {POPL},
  year      = {2011},
  pages     = {105-118}
}
@inproceedings{Logozzo-VMCAI07,
  author    = {Logozzo, F{.}},
  title     = {Cibai: An Abstract Interpretation-Based Static Analyzer
               for Modular Analysis and Verification of Java Classes},
  booktitle = {VMCAI},
  year      = {2007},
  pages     = {283-298}
}
@inproceedings{LogozzoFahndrich08,
  author    = {Logozzo, F{.} and
               F{\"a}hndrich, M{.}},
  title     = {Pentagons: a weakly relational abstract domain for the efficient
               validation of array accesses},
  booktitle = {SAC},
  year      = {2008},
  pages     = {184-188}
}
@inProceedings{LogozzoFahndrich11, 
   author    = {Logozzo, F{.} and
               F{\"a}hndrich, M{.}},
  title = 	 {Checking Compatibility of Bit Sizes in Floating Point Comparison Operations},
  year = 	 {2011},
  booktitle = {3rd workshop on Numerical and Symbolic Abstract Domains},
  series = 	 {ENTCS}
}


@InProceedings{PerkinsEtAl09,
  author = 	 {Perkins, J{.} H{.} and  Kim, S{.} and  Larsen, S{.} and  Amarasinghe, S{.} P{.} and   Bachrach, J{.} and   Carbin, M{.} and   Pacheco, C{.} and   Sherwood, F{.} and  Sidiroglou, S{.} and   Sullivan, G{.} and   Wong, W{.}-F{.} and   Zibin, Y{.} and  Ernst, M{.} D{.} and  Rinard, M{.}},
  title = 	 {Automatically patching errors in deployed software},
  booktitle = {{ACM SOSP}},
  year = 	 {2009}
}

@inproceedings{FahndrichLeino03,
  author    = {F{\"a}hndrich, M{.} and
               Leino, K{.} R{.} M{.}},
  title     = {Declaring and checking non-null types in an object-oriented
               language},
  booktitle = {{ACM OOPSLA}},
  year      = {2003},
}
@inproceedings{Fahndrich10,
  author    = { F{\"a}hndrich, M{.}},
  title     = {Static Verification for {C}ode {C}ontracts},
  booktitle = {SAS},
  year = 2010
}
@article{LiskovWing94,
  author    = {Liskov, B{.} and
               Wing, J{.} M{.}},
  title     = {A Behavioral Notion of Subtyping},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {16},
  number    = {6},
  year      = {1994},
}

@article{MeyerIEEEComputer92,
  author    = {Meyer, B{.}},
  title     = {Applying "{D}esign by {C}ontract"},
  journal   = {IEEE Computer},
  volume    = {25},
  number    = {10},
  year      = {1992},
  pages     = {40-51},
}

@inproceedings{ChandraFS09,
  author    = {Chandra, S{.} and
               Fink, S{.} J{.} and
               Sridharan. M{.}},
  title     = {Snugglebug: a powerful approach to weakest preconditions},
  booktitle = {PLDI},
  year      = {2009},
  pages     = {363-374}
}

@inproceedings{BallKY05,
  author    = {Ball, T{.} and
               Kupferman, O{.} and
               Yorsh, G{.}},
  title     = {Abstraction for Falsification},
  booktitle = {CAV},
  year      = {2005},
  pages     = {67-81}
}

@inproceedings{GodefroidLM08,
  author    = { Godefroid, P{.} and
               Levin, M{.} Y{.} and
               Molnar, D{.} A{.}},
  title     = {Automated Whitebox Fuzz Testing},
  booktitle = {NDSS},
  year      = {2008}
}

@inproceedings{ChandraPLDI2009,
 author = {Chandra, S{.} and Fink, S{.} J{.} and Sridharan, M{.}},
 title = {Snugglebug: a powerful approach to weakest preconditions},
 booktitle = {Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation},
 series = {PLDI '09},
 year = {2009},
 pages = {363--374}
}

@article{PezzeEtAl11,
  author    = { Pezz{\`e}, M{.} and
               Rinard, M{.} C{.} and
               Weimer, W{.} and
                Zeller, A{.}},
  title     = {Self-Repairing Programs (Dagstuhl Seminar 11062)},
  journal   = {Dagstuhl Reports},
  volume    = {1},
  number    = {2},
  year      = {2011},
  pages     = {16-29}
}

@inproceedings{WeimerEtAl09,
  author    = {Weimer, W{.} and
               Nguyen, T{.} and
               Le Goues, C{.} and
               Forrest, S{.}},
  title     = {Automatically finding patches using genetic programming},
  booktitle = {ICSE},
  year      = {2009}
}

@inproceedings{Pex,
  author    = { Tillmann, N{.} and
               de Halleux, J{.}},
  title     = {Pex-White Box Test Generation for .NET},
  booktitle = {TAP},
  year      = {2008}
}

@inproceedings{WeiEtAl,
  author    = {Wei, Y{.} and
               Pei, Y{.} and
               Furia, C{.} A{.} and
               Silva, L{.} S{.} and
               Buchholz, S{.} and
               Meyer, B{.} and
               Zeller, A{.}},
  title     = {Automated fixing of programs with contracts},
  booktitle = {ISSTA},
  year      = {2010},
  pages     = {61-72}
}

@inproceedings{SamantaEtAl08,
  author    = {Samanta, R{.} and
               Deshmukh, J{.} V{.} and
               Emerson, E{.} A{.}},
  title     = {Automatic Generation of Local Repairs for Boolean Programs},
  booktitle = {FMCAD},
  year      = {2008},
}

@inproceedings{JobstmannEtAl05,
  author    = {Jobstmann, B{.} and
               Griesmayer, A{.} and
                Bloem, R{.}},
  title     = {Program Repair as a Game},
  booktitle = {CAV},
  year      = {2005}
}


@inproceedings{GriesmayerEtAl06,
  author    = {Griesmayer, A{.} and
               Bloem, R{.} and
               Cook, B{.}},
  title     = {Repair of Boolean Programs with an Application to C},
  booktitle = {CAV},
  year      = {2006}
}

@Misc{roslyn,
  author = 	 {Microsoft},
  title = 	 {Roslyn {CTP}},
  howpublished = {\texttt{http://msdn.microsoft.com/en-us/roslyn}},
  year = 	 {2011}
}



@Misc{eclipse,
  title = 	 {Eclipse},
  howpublished = {\texttt{http://eclipse.org}},
  year         = {2011},
}

@Misc{MSIL,
  author = 	 {{ECMA}},
  title = 	 {Standard {ECMA-355}, {C}ommon {L}anguage {I}nfrastructure },
  month = 	 jun,
  year = 	 {2006},
  howpublished = {\url{http://www.ecma-international.org/publications/standards/Ecma-335.htm}},
}

@Misc{MSBuild,
  author = 	 {Microsoft},
  title = 	 {Standard {ECMA-355}, {C}ommon {L}anguage {I}nfrastructure },
  month = 	 jun,
  year = 	 {2006},
  howpublished = {\url{http://msdn.microsoft.com/en-us/library/0k6kkbsd.aspx}},
}

@Misc{make,
  author = 	 {Stuard Feldman},
  title = 	 {Unix Make Tool},
  howpublished = {\url{http://en.wikipedia.org/wiki/Make_(Unix)}},
}

@Article{JML,
  Author =	 "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  Title =	 "Preliminary Design of {JML}: A Behavioral Interface Specification Language for {Java}",
  journal = "SIGSOFT",
  volume = 31,
  number = 3,
  month = mar,
  year = 2006,
  pages = {1-38},
  URL = {http://doi.acm.org/10.1145/1127878.1127884},
  publisher = "ACM",
}


@InProceedings{SpecSharp,
  Author="Mike Barnett and K. Rustan M. Leino and Wolfram Schulte",
  Title="The {Spec\#} programming system: An overview.",
  Booktitle="CASSIS",
  Year=2004,
  Series="LNCS",
  volume=3362,
  publisher="Springer",
}

@inproceedings{cccheck,
author = {F{\"a}hndrich, M{.} and Logozzo, F{.}},
title = {Static Contract Checking with Abstract Interpretation},
booktitle = {FoVeOOS},
year = {2010},
pages = {10-30}
}

@TechReport{eclipse-jmlc,
  author =       {Amritam Sarcar and Yoonsik Cheon},
  title =        {A New Eclipse-Based JML Compiler Built Using AST Merging},
  institution =  {University of Texas at El Paso},
  year =         2010,
  number =    {TR \#10-08}}



@InProceedings{openJML,
  author =       {David Cok},
  title =        {{OpenJML}: {JML} for {Java} 7 by {Extending} {OpenJDK}},
  booktitle =    {NASA Formal Methods},
  pages =     {472--479},
  publisher = {Springer},
  year =      2011,
  volume =    6617,
  series =    {LNCS},
  month =     mar
}

@book{Eclipse-book,
 author = {McAffer, Jeff and Lemieux, Jean-Michel},
 title = {Eclipse Rich Client Platform: Designing, Coding, and Packaging Java(TM) Applications},
 year = {2005},
 isbn = {0321334612},
 publisher = {Addison-Wesley Professional},
} 

@InProceedings{JMLtools,
  author =       {Lilian Burdy and Yoonsik Cheon and David Cok and Michael Ernst and Joe Kiniry and Gary T. Leavens and Leino, K. Rustan M. and Erik Poll},
  title =        {An overview of {JML} tools and applications},
  booktitle =    {International Journal on Software Tools for Technology Transfer},
  pages =     {212--232},
  publisher = {Springer},
  year =      2005,
  volume =    7,
  number =    3,
  month =     jun
}
